x:Id, k:Knd, ds:x:Id fp Type, da:a:Knd fp Top, f:Top, x1:Id, L:Knd List, t:Type.
ds || x1 : t
 (x = x1  (k  L))
 (only members of L affect x1 :t ||+ with declarations ds:dsda:daeffect of k(v) is x := f s v) 

latex

Definitions

x:A. B(x), P  Q, f || g, x : v, A ||+ B, only members of L affect x :t, with declarations ds:dsda:daeffect of k(v) is x := f s v, P & Q, M1 || M2, ma-frame-compatible(A;B), mk-ma, , M1 ||decl M2, 1of(t), 2of(t), Prop, b, x  dom(f), f(x), deq-member(eq;x;L), reduce(f;k;as), false, Y, if b t else f fi, t  T, ma-frame-compat(A;B), xdom(f). v=f(x)   P(x;v), M.rframe(A.pre p for a), M.frame(k affects x), M.aframe(k affects x), M.rframe(A.effect f of k on y), M.sframe(k sends <l,tg>), M.rframe(A.sends tfL of k on l), P  Q, P  Q, z != f(x)  P(a;z), P  Q, x. t(x), a:A fp B(a), False, x(s), a = b

Lemmas

assert wf, deq-member wf, assert of bor, or functionality wrt iff, false wf, deq property, assert-deq-member, Kind-deq wf, pi1 wf, iff transitivity, bor wf, eq id wf, pi2 wf, bfalse wf, assert-eq-id, l member wf, eqof wf, Id wf, Knd wf, fpf-compatible wf, id-deq wf, fpf-single wf, top wf, fpf wf